Add context-sensitive DSA with per-function memory regions by shaobo-he · Pull Request #810 · smackers/smack

shaobo-he · 2026-03-30T04:24:00Z

Implement CS-DSA per-function region computation with call-site mapping for Boogie parameterized memory. Each function computes its own region vector and call sites map callee regions to caller regions. Add CS-DSA design doc.

Implement CS-DSA-based per-function region analysis replacing the single global region vector. Each function gets its own region vector computed from its CS graph, with call-site mappings connecting callee regions to caller regions. Key components: - Per-function region vectors in Regions with call-site mappings - DSA link-following to discover heap node correspondences across calls - Top-down and bottom-up region merge propagation for soundness - Phase 1 link-following to pre-create regions for pointer-reachable nodes - Region(Node*) constructor for creating regions from DSA nodes - Parameter mapping priority over global mapping in mergeCalleeRegion - VProperty.__members__ fix for --check memory-safety flag - Index pointer return values from all calls (not just declarations) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

- Add return value mapping to call-site mappings (fixes func_ptr2) - Create missing caller regions via Region(Node*) during link-following - Iterate computeCallSiteMappings to propagate regions up the call chain - Index pointer return values from all calls, not just declarations - Remove broken identity fallback (callerR = calleeR) - Update cs-dsa-memory-plan.md to reflect final architecture Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

shaobo-he

Audit: ntdrivers performance regression + region-bookkeeping soundness issues

I audited this PR against develop with a focus on the c/ntdrivers slowdown (builds of both branches, all 7 benchmarks, SMACK's exact default flags: --mem-mod=no-reuse-impls --verifier=corral, /k:1 /recursionBound:1 /maxStaticLoopBound:1 /useProverEvaluate, 600s limit). Summary of results, then confirmed code issues.

1. The regression, reproduced

Verdicts agree with develop on all 7 benchmarks; wall time does not:

benchmark	develop	this PR	ratio
cdaudio_true	31.7s	211.9s	6.7×
floppy2_true	26.6s	184.2s	6.9×
parport_true	56.7s	164.3s	2.9×
diskperf_true	17.2s	23.5s	1.4×
diskperf_false	11.0s	15.2s	1.4×
kbfiltr_false	15.2s	20.0s	1.3×
parport_false	19.6s	20.1s	1.0×

The _false cases barely move because Corral stops at the first confirmed bug; the _true cases must exhaust the search. cdaudio at ~212s also explains the intermittent ntdrivers CI failures (600s limit on slower CI machines).

2. Root cause: parameterized memory bypasses Corral's variable abstraction

Corral's CEGAR abstraction applies to globals only: it lazily grows a tracked-variable set and havocs everything else. On develop, that set converges to only 10–18 of 38–102 $M globals per ntdrivers benchmark — most memory maps are never reasoned about at all. On this branch, non-entry procedures carry maps as parameters/returns (e.g. cdaudio's _BLAST_init: 15 map inputs + 15 map outputs, plus 632 prologue/epilogue whole-map copies across the file). Parameters are invisible to the abstraction machinery, so all of that dataflow is fully precise from round one.

Corral's own stats isolate it: on cdaudio_true, refinement rounds (13 vs 14) and procedures inlined (228 vs 232) are essentially identical, but Time spent checking a program goes 25s → 204s (8×). The regression is per-VC cost, not CEGAR loop length.

3. Can we fix it on the Corral side? (tested: no)

config	cdaudio_true	floppy2_true	parport_true	parport_false
dev default	31.7	26.6	56.7	19.6
dev `/trackAllVars`	30.4	462.6	435.3	42.6
dev `/useArrayTheory`	30.3	33.8	62.3	19.7
cs default	211.9	184.2	164.3	20.1
cs `/trackAllVars`	114.1	580.7	506.9	66.0
cs `/useArrayTheory`	270.3	155.2	193.4	19.3

No existing Corral flag helps consistently. Corral 1.1.8 simply has no mechanism to abstract map-valued parameters; extending the tracked-variable CEGAR to a parameterized-memory calling convention would be new Corral feature work.

Suggested direction instead (SMACK-side): regions already carry a globalScope bit. Keep global-backed regions as Boogie globals for all procedures (that is exactly the state Corral abstracts well, and in CIL-processed drivers nearly all long-lived state is global structs), and thread only function-private / parameter-reachable heap regions through signatures. This keeps the CS-DSA precision win while restoring Corral's abstraction lever, and would also unblock the pthread suites (Corral's concurrency handling needs shared globals for context switching, which is why they had to be disabled here). Gating parameterized memory behind an option would let -sea-dsa=cs land independently.

4. Confirmed code issues (adversarially verified)

Critical — soundness:

Index-shift corruption in plain Regions::idx() (lib/smack/Regions.cpp:405-436): idx() can merge and erase() regions, shifting indices, but unlike mergeCalleeRegion it remaps nothing — funcRegions read/modified sets (recorded in Phase 2), callSiteMappings, and mergedRegionAliases silently go stale. Phase 3 (computeOneCallSiteMapping, line 633) and even Boogie-generation-time code (SmackRep.cpp:302,315,335,360,400,456,532,554,1408) call this mutating idx() after bookkeeping is frozen. Consequence: writes attributed to the wrong $M.r, or writes not threaded out at all. The Phase-3 convergence check compares only total region counts, so one merge (−1) plus one creation (+1) in the same pass exits the loop with stale mappings.

Major — soundness:

Stale by-value copy in computeOneCallSiteMapping (Regions.cpp:617-634): the callee region vector is copied before a loop whose idx() calls can mutate the underlying vectors; self-recursive calls corrupt their own mapping, and earlier entries of the local mapping are not repaired after a mid-loop merge.
Bottom-up pass merges on representative-node equality alone (Regions.cpp:872-894): disjoint-offset caller regions on the same DSA node get merged, systematically destroying field sensitivity for driver-style structs and nulling map types toward [ref] i8 (25% of map decls in the cdaudio BPL). Also a perf contributor. repToMappedCaller[rep] = m.second is additionally last-write-wins when several mapped caller regions share a node.
InvokeInst is invisible to every Regions phase (Regions.cpp:214,579,728,960 all dyn_cast<CallInst>): SmackRep::call then does dyn_cast<const CallInst> (SmackRep.cpp:1170), gets the empty mapping, and hits llvm_unreachable (SmackRep.cpp:1176) — a crash in Debug and UB in Release for C++/Rust invokes of any callee with interface regions; if the callee has no interface regions the invoke silently loses read/write propagation instead.
propagateRegionMerges is superlinear (Regions.cpp:794-906): every single merge rescans all module call-site mappings, with break-and-restart fixpoints on top. Translation is still ~1s on ntdrivers today, so this is a scaling landmine rather than the current bottleneck.

Minor but worth noting: the __SMACK_code("call foo(...)") string-rewriting heuristic (SmackRep.cpp:1206-1337) can silently leave arity-mismatched calls when its LLVM call-site matching fails; llvm_unreachable for a missing call-site mapping is a Release-build UB path (should be report_fatal_error).

Non-issues we checked and ruled out (so nobody chases them): the per-function $M.r shadows are procedure-local variables (no module-level name collisions), and the absent modifies clauses match develop behavior (Corral infers modsets; Boogie gets /doModSetAnalysis).

5. Recommended plan

Fix the mechanical soundness issues above (fixes incoming).
Rework the memory interface so globalScope regions stay Boogie globals for all procedures; thread only non-global regions. Re-measure ntdrivers.
Keep parameterized memory behind a flag until (2) lands, so CS-DSA precision isn't tied to the calling-convention change.
Revisit the disabled CI suites afterwards — pthread specifically should come back with (2).

_{🤖 Audit assisted by Claude Code: dual-build benchmark reproduction + multi-agent adversarially-verified code review.}

Fixes for the issues found in the PR 810 audit (see the PR review comment for the full findings). Region bookkeeping: - Route idx() cascade merges through remapAfterMerge (extracted from mergeCalleeRegion) so read/modified sets, call-site mappings (both sides for self-recursive call sites), merged-region aliases, and global-memory mappings are repaired whenever a merge erases a region and shifts indices. Previously these silently went stale, attributing accesses to the wrong $M region. - Build call-site mappings in place so merges triggered mid-computation repair already-inserted entries; iterate the live callee region vector with a per-iteration copy instead of a stale whole-vector copy. - Replace the count-based Phase 3 convergence check, which exits early when one merge and one creation in the same pass cancel out, with a structural-version check; raise the pass cap from 10 to 100 and warn on non-convergence. - Clamp node-derived region lengths to at least one byte: zero-length regions from never-dereferenced DSA nodes are empty intervals that overlap nothing (not even an identical probe), so every Phase 3 pass re-created them and the fixpoint never converged. - Make region hull arithmetic 64-bit and saturating; the 32-bit offset + length wrap-around for unbounded-length regions made extents non-monotonic under merging, another convergence blocker. - Bounds-check the Phase 1 link-following loop against mid-loop erases. - Count and report call-site mapping associations dropped by key collisions after Phase 3 convergence (1165 on cdaudio_true); affected callers may see stale memory. The keep-priority drop policy is pre-existing; the warning makes it observable until a cascading caller-side merge is implemented. Invoke support: - Key call-site mappings on CallBase and handle invokes in all Regions phases and SmackRep::call; previously an invoke of a function with interface regions hit llvm_unreachable (undefined behavior in release builds), and invokes of functions without them silently lost read/write propagation. - Fix vararg procedure naming for invokes (the argument count came from getNumOperands() - 1, which includes the invoke's destination operands), and find vararg call sites through invokes in findCallers. - Resolve bitcast/aliased direct callees in visitInvokeInst the same way visitCallInst does. Robustness: - Replace llvm_unreachable with report_fatal_error on unmappable call sites and missing region mappings so release builds fail loudly instead of invoking undefined behavior. Validation: 2052 regression configurations pass (--exhaustive over c/basic, c/data, c/ntdrivers-simplified, c/targeted-checks, c/special, c/strings, c/locks, c/bits, c/float, c/unroll); ntdrivers BPL output is unchanged except for the removal of phantom threaded maps, with identical Corral verdicts and neutral verification time; a C++ invoke smoke test now verifies end to end (and its negation reports an error). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

PR 810 threads memory maps through procedure signatures ($M.r.in parameters, $M.r.out returns). Corral's variable-tracking abstraction only applies to global variables, so every threaded map is fully precise in every VC whether or not the property needs it, and each inlined instance carries map parameters and whole-map copies. On c/ntdrivers this made verification up to 6.9x slower than develop (cdaudio_true 32s -> 212s), with Corral's own statistics showing the regression entirely in per-VC solving time. This change binds all cross-function memory to module-level maps: - Phase 3.6 (computeGlobalMemoryMappings, reworked): every function's global-backed regions map to the entry function's region for the same global; conflicting targets merge the entry regions (mergeCalleeRegion repairs all bookkeeping); the entry region absorbs each function's attribute view and is forced module-level. - Phase 3.7 (unifySharedRegions, new): a union-find over (function, region) pairs linked by call-site mappings and the global mappings unifies the remaining cross-function memory. Classes containing an entry region bind every member to that entry map; entry-less classes with two or more members get a synthetic module-level map ($M.S.k); single-member classes stay procedure-local. Two entry regions in one class alias through some call chain and are merged. - Emission resolves every region through SmackRep::resolveRegion to the owning map (entry map $M.g, shared map $M.S.k, or procedure-local shadow $M.L.r, a separate namespace to avoid colliding with the module-level names) and uses the resolved region's attributes for map types and load/store/memcpy/memset/vector operations. Interface threading survives only for regions with no module-level binding (e.g. in functions never called through a mapped call site). - Multiple defined entry points are rejected with a hard error: the unified numbering follows the first entry point, and a second entry would silently verify against the wrong maps (this was already inconsistent under threading; now it is loud). Measured on c/ntdrivers (wall seconds, corral, default flags): develop PR 810 unified cdaudio_true 31.7 211.9 30.8 floppy2_true 26.6 184.2 29.0 parport_true 56.7 164.3 50.1 all 7 total 178.0 639.2 186.6 with identical verdicts everywhere. The unified build also keeps more memory maps than develop (e.g. floppy2 71 vs 38): CS-DSA's finer region splitting survives; only its calling-convention change is rolled back. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

shaobo-he · 2026-07-09T05:54:49Z

Follow-up: soundness fixes + ntdrivers regression resolved

Two commits pushed, addressing the issues from the audit review above.

`4e9fa364` — region bookkeeping soundness + invoke support

All region merges now go through a shared remapAfterMerge that repairs read/modified sets, call-site mappings (both sides for self-recursive call sites), merged-region aliases, and global-memory mappings. Previously idx() cascade merges silently corrupted every index-keyed structure (the critical audit finding).
Phase 3 convergence is version-based instead of count-based (a merge plus a creation in one pass no longer fakes convergence). This exposed two real convergence blockers the old check masked, both fixed: zero-length regions from never-dereferenced DSA nodes (empty intervals match nothing, so they were re-created every pass), and 32-bit offset + length wrap-around making merged extents non-monotonic. Phase 3 now converges in ~2 passes on ntdrivers.
InvokeInst is handled throughout (CallBase generalization): previously invokes of functions with interface regions hit llvm_unreachable (UB in release builds). Includes vararg proc naming for invokes, findCallers through invokes, and the bitcast-callee fallback in visitInvokeInst. Verified end-to-end with a C++ try/catch test.
Mapping associations dropped by post-convergence key collisions are now counted and reported (SMACK warning: N call-site region mapping(s) dropped...) — 1165 on cdaudio_true, worth keeping an eye on.

`737bc606` — emit cross-function memory as module-level maps

This resolves the ntdrivers regression. Corral's variable-tracking abstraction applies to globals only, so threaded map parameters were fully precise in every VC, and each inlined instance carried map params plus whole-map copies. Corral's stats put the entire regression in per-VC solve time (cdaudio: same 13 refinement rounds, same ~220 inlinings, but 25s → 204s in program checks).

The fix unifies all cross-function memory into module-level maps via a union-find over the call-site mappings (entry-function maps $M.g where a class reaches the entry, synthetic $M.S.k maps otherwise); only function-private regions remain procedure-local ($M.L.r, a separate namespace). Threading survives only for regions with no module-level binding.

Measured (wall seconds, corral, default flags):

benchmark	develop	before	after
cdaudio_true	31.7	211.9	25.7
floppy2_true	26.6	184.2	24.1
parport_true	56.7	164.3	50.4
all 7 ntdrivers	178	639	~180

Identical verdicts everywhere. Note the CS-DSA precision win survives: the unified build keeps more distinct memory maps than develop (floppy2: 71 vs 38) — only the parameterized calling convention is rolled back.

Validation: 2052 regression configurations (--exhaustive over c/basic, data, ntdrivers-simplified, targeted-checks, special, strings, locks, bits, float, unroll) pass with zero failures.

Notes / follow-ups

Multiple --entry-points now fail loudly with report_fatal_error: unified numbering follows the first entry point, and a second entry would silently verify against the wrong maps (adversarial review produced a concrete wrong-verdict repro; this was already inconsistent under threading, just quieter). Only one regression test uses --entry-points, single-entry, unaffected.
Since shared memory is global again, the pthread suites are likely re-enableable — Corral's context switching needs shared globals, which was why they were disabled. Worth trying before merge; contracts/memory-safety still need their own look.
Calls from __SMACK_init_func_* bodies to region-threaded callees have a pre-existing numbering inconsistency (not reachable in C flows; documented here for the record).

_{🤖 Fixes and benchmarks with Claude Code; each change adversarially reviewed by a multi-agent workflow and validated against the full regression suites.}

The CI run caught test/c/data/two_arrays1.c timing out under the no-reuse and reuse memory models: the shared-memory union-find fused the two arrays through their common callee's formal parameter (array1 ~ formal ~ array2), collapsing memory that both the threading scheme and develop keep separate, and making the merged map 4x more expensive to reason about (192s vs 43s locally). A class now keeps the per-call-site threading when some function has exactly two distinct regions in it: that is deliberate program structure (two objects flowing through one callee), and merging loses real separation. Classes where a function has three or more regions are DSA-collapse artifacts (11-198 duplicated members on the ntdrivers benchmarks); threading those costs far more than the separation is worth, so they still bind to module-level maps. Regions bound by globals identity in Phase 3.6 keep their binding even inside threaded classes: sea-dsa propagates global symbols along call chains, so a bound callee implies a bound caller and the mix stays consistent. Measured: two_arrays1 40.7s (develop: 51.4s; unguarded merge: 192s); ntdrivers unchanged within noise (all 7: 192s vs develop 178s, same verdicts); all 2052 regression configurations pass. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

shaobo-he · 2026-07-09T06:55:06Z

CI c/data timeout — fixed in `404f5e1d`

The two_arrays1.c timeout (no-reuse/reuse, 180s regtest limit) was a precision loss in the memory unification: the union-find fused the two arrays through their common callee's formal (array1 ~ formal ~ array2), collapsing memory that both the threading scheme (~92s CI) and develop (~105s CI) keep separate, which made the merged map ~4x harder for Corral.

The fix keeps per-call-site threading for union classes where some function has exactly two distinct regions (deliberate program structure — two objects through one callee), while classes with three or more same-function regions (DSA-collapse artifacts spanning 11–198 members on ntdrivers) still bind to module-level maps. Globals-identity bindings are kept even inside threaded classes (sea-dsa propagates global symbols along call chains, so a bound callee implies a bound caller).

Re-measured:

two_arrays1: 40.7s locally (develop: 51.4s; before the fix: 192s)
ntdrivers, all 7: 192s total vs develop's 178s, identical verdicts (cdaudio_true 29.4s, floppy2_true 33.1s, parport_true 62.4s)
all 2052 regression configurations pass locally

_{🤖 Diagnosed and fixed with Claude Code.}

The context-sensitive pipeline produced *coarser* memory maps than the context-insensitive baseline (hid-waltop: 39 module maps vs develop's 214), defeating its own purpose and slowing verification up to 18x on LDV driver benchmarks. Phase-wise instrumentation located the losses: - Phase 1 pre-seeded formals, call arguments, globals, and pointer call returns with whole-pointee-extent regions; each such probe overlaps and absorbs every field region on its node (a whole-global probe run per function collapsed __SMACK_static_init's 737 field regions to ~40). These probes were a workaround for call-site mappings mutating region indices, which the bookkeeping-repair machinery has since made safe: regions are now created from actual accesses only, and memory reached through calls gets field-precise regions from the call-site mapping fixpoint. The link-following closure (whole-node regions) is removed for the same reason; pointer-return probes remain only for external functions. - The bottom-up pass of propagateRegionMerges merged caller regions on representative-node equality, folding disjoint fields. It is replaced by an overlap-only normalization sweep (same predicate idx() uses), run again after Phases 3.6-3.7 since merges can widen extents without re-checking neighbors. - __SMACK_static_init and __SMACK_init_func* bodies are emitted in the entry function's region context, but their region probes previously fell back to the underlying global, collapsing every field to its base. Their cells are now translated from their own DSA graph into the entry graph through a globals-seeded SimulationMapper, composing offsets with sea-dsa's cell semantics (collapsed nodes fold to zero, array nodes wrap modulo the node size); the same translation backs cross-function lookups in DSAWrapper. Globals no access covers are anchored in the entry vector so module maps keep at least per-global granularity. - Region::mergeAttributes absorbs only emission-relevant attributes (type, singleton, bytewise); absorbing the matching flags (incomplete/complicated/collapsed) armed spurious cross-node merges after normalization, and one such post-pass merge left an already-emitted map reference dangling. - isExternal no longer probes regions (a whole-pointee probe at translation time could merge field regions late); it asks the DSA node directly. computeGlobalMemoryMappings lookups are now non-mutating (findRegion). The threading guard for paired regions additionally requires a small class, since field-granular classes made the multiplicity test fire on large collapse artifacts. Measured (corral, wall seconds): develop before after module maps (dev) hid-waltop 43_1a 2.0 37.2 1.9 214 (214) two_arrays1 51.4 40.7 24.5 cdaudio_true 31.7 29.4 29.1 70 (52) parport_true 56.7 62.4 60.5 108 (102) floppy2_true 26.6 33.1 105.9 46 (38) with identical verdicts everywhere; all 2052 regression configurations pass. floppy2's residual comes from its per-function access patterns (memset/whole-struct operations), not the region pipeline, and is left as a follow-up. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

shaobo-he · 2026-07-10T16:03:30Z

Region granularity restored: CS now produces finer maps than develop (`76165f71`)

Following up on the LDV slowdowns (hid-waltop et al.): those traced to the CS pipeline producing coarser maps than develop — hid-waltop had 39 module maps where develop has 214. Phase-wise instrumentation found four independent coarsening mechanisms, all fixed:

Whole-extent anchor probes. Phase 1 pre-seeded formals, call args, globals, and pointer returns with whole-pointee extents; each probe absorbs every field region on its node (a per-function whole-global probe collapsed __SMACK_static_init's 737 field regions to ~40). These were a workaround for the index-corruption bug fixed earlier; regions now come from actual accesses only, with call-reached memory created field-precisely by the mapping fixpoint. The whole-node link-following closure is gone too.
Rep-equality bottom-up merging folded disjoint fields; replaced with an overlap-only normalization sweep (also run after Phases 3.6–3.7, where merges can widen extents without rechecking neighbors).
Static-init offset loss. __SMACK_static_init emits in the entry region context, but its probes fell back to the underlying global, collapsing fields to the base. Its cells are now translated from its own DSA graph into the entry graph via a globals-seeded SimulationMapper, composing offsets with sea-dsa's cell semantics — collapsed nodes fold to zero, array nodes wrap modulo node size (missing that wrap scattered struct_array/strings-suite initializers into phantom regions).
Attribute absorption armed spurious merges: mergeAttributes now carries only emission-relevant attributes (type/singleton/bytewise), not the overlaps() matching flags, whose cross-node propagation caused one post-emission merge that left a dangling $M reference.

Results (corral, wall seconds):

	develop	before	after	maps (dev)
hid-waltop 43_1a	2.0	37.2	1.9	214 (214)
two_arrays1	51.4	40.7	24.5	—
cdaudio_true	31.7	29.4	29.1	70 (52)
parport_true	56.7	62.4	60.5	108 (102)
floppy2_true	26.6	33.1	105.9	46 (38)

Identical verdicts everywhere; all 2052 regression configurations pass. two_arrays1 is now 2x faster than develop — array and field separation preserved — which is the CS payoff this PR was after.

Known follow-up: floppy2's residual comes from its per-function access patterns (whole-struct memset/memcpy), not the region pipeline. The dumpPhase/SMACK_DEBUG_PHASES instrumentation is left in (env-gated) for future granularity work.

_{🤖 Diagnosed and fixed with Claude Code.}

floppy2_true still ran 4x slower than develop after the granularity fixes, with an identical CEGAR trajectory (same rounds, same tracked variables, same inlinings) but 4x the per-VC solving time. The structural difference: fine-grained regions produce many single-member classes, which stayed procedure-local maps — and Corral's variable-tracking abstraction applies to global variables only. An untracked global map is havoced for free; a procedure-local map is fully precise in every inlined instance, unconditionally. Local maps are strictly worse than globals under Corral. All regions now get module-level maps: single-member classes and regions outside every mapping bind to shared maps, and the entry function's own regions are all module-level (this is develop's memory layout, at context-sensitive granularity). Procedure-local shadows remain only for the threaded classes, which need .in/.out copies. Boogie and Corral infer the modifies sets. Measured (corral, wall seconds): develop before after floppy2_true 26.6 105.9 39.9 parport_true 56.7 60.5 50.2 cdaudio_true 31.7 29.1 27.4 all 7 ntdrivers 178 ~250 176.5 hid-waltop 43_1a 2.0 1.9 1.8 two_arrays1 51.4 24.5 28.0 The 7-benchmark ntdrivers total now beats develop. All verdicts unchanged; all 2052 regression configurations pass. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

shaobo-he · 2026-07-10T16:22:13Z

floppy2 fixed: local maps are strictly worse than globals under Corral (`0d6524ac`)

The floppy2 residual had a surprising root. Its CEGAR trajectory was identical to the fast configurations — same 8 rounds, same 7 tracked variables, same ~190 inlinings — but per-VC solve time was 4x. The structural delta: the granularity work produced many single-member region classes, which stayed procedure-local maps (22 → 59 locals). Corral's variable-tracking abstraction applies to globals only: an untracked global map is havoced for free, while a procedure-local map is fully precise in every inlined instance, unconditionally. So a "private" local map is strictly more expensive than an unabstracted global — the opposite of the intuition that motivated locals.

Every region now gets a module-level map (develop's layout, at CS granularity); procedure-local shadows survive only for the threaded classes that need .in/.out copies. Corral decides per-property what to track.

	develop	before	after
floppy2_true	26.6	105.9	39.9
parport_true	56.7	60.5	50.2
cdaudio_true	31.7	29.1	27.4
all 7 ntdrivers	178.0	—	176.5
hid-waltop 43_1a	2.0	1.9	1.8
two_arrays1	51.4	24.5	28.0

The ntdrivers total now beats develop, with context-sensitive granularity (e.g. two_arrays1 keeps both arrays and their fields separate — ~2x faster than develop). All verdicts unchanged; all 2052 regression configurations pass.

_{🤖 Diagnosed and fixed with Claude Code.}

shaobo-he force-pushed the cs branch 2 times, most recently from 2385908 to bbf0148 Compare March 31, 2026 05:44

shaobo-he force-pushed the cs branch from bbf0148 to df73bd9 Compare March 31, 2026 05:52

shaobo-he and others added 10 commits March 30, 2026 22:54

Fix formatting

fab4750

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Merge branch 'develop' into cs

812378d

Fix context-sensitive DSA region threading

098c3d4

Apply clang-format to regions pass

35d414f

Temporarily disable incompatible CI suites

983a542

Preserve aliases for merged DSA regions

3cd18b1

Preserve region types during call-site mapping

efc8fe1

Thread memory through inline SMACK calls

f751018

Terminate reachable region closure on stable size

71c48e2

shaobo-he commented Jul 8, 2026

View reviewed changes

shaobo-he and others added 2 commits July 8, 2026 15:59

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Add context-sensitive DSA with per-function memory regions#810

Add context-sensitive DSA with per-function memory regions#810
shaobo-he wants to merge 16 commits into
developfrom
cs

shaobo-he commented Mar 30, 2026

Uh oh!

shaobo-he left a comment

Uh oh!

shaobo-he commented Jul 9, 2026

Uh oh!

shaobo-he commented Jul 9, 2026

Uh oh!

shaobo-he commented Jul 10, 2026

Uh oh!

shaobo-he commented Jul 10, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

shaobo-he commented Mar 30, 2026

Uh oh!

shaobo-he left a comment

Choose a reason for hiding this comment

Audit: ntdrivers performance regression + region-bookkeeping soundness issues

1. The regression, reproduced

2. Root cause: parameterized memory bypasses Corral's variable abstraction

3. Can we fix it on the Corral side? (tested: no)

4. Confirmed code issues (adversarially verified)

5. Recommended plan

Uh oh!

shaobo-he commented Jul 9, 2026

Follow-up: soundness fixes + ntdrivers regression resolved

4e9fa364 — region bookkeeping soundness + invoke support

737bc606 — emit cross-function memory as module-level maps

Notes / follow-ups

Uh oh!

shaobo-he commented Jul 9, 2026

CI c/data timeout — fixed in 404f5e1d

Uh oh!

shaobo-he commented Jul 10, 2026

Region granularity restored: CS now produces finer maps than develop (76165f71)

Uh oh!

shaobo-he commented Jul 10, 2026

floppy2 fixed: local maps are strictly worse than globals under Corral (0d6524ac)

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

`4e9fa364` — region bookkeeping soundness + invoke support

`737bc606` — emit cross-function memory as module-level maps

CI c/data timeout — fixed in `404f5e1d`

Region granularity restored: CS now produces finer maps than develop (`76165f71`)

floppy2 fixed: local maps are strictly worse than globals under Corral (`0d6524ac`)